; COMMAND-LINE: --produce-proofs
; EXPECT: unsat
(set-logic ALL)
(set-info :status unsat)
(declare-fun a () String)  
(declare-fun b () String) 
(declare-fun c () Bool) 
(declare-fun d () Bool) 
(declare-fun g () Bool) 
(declare-fun e () Bool) 
(declare-fun f () String)       
(assert (= b  f)) 
(assert (= c (= "" b))) 
(assert (= d (not c))) 
(assert d)  
(assert (= a f))   
(assert (= g (not (= e (not (= "" a)))))) 
(assert g)     
(assert e) 
(check-sat)  
